The next talk in the Galois Tech Seminar series:

• Date: Tuesday, October 13th, 2009
• Title: Constructing A Universal Domain for Reasoning About Haskell Datatypes
• Speaker: Brian Huffman
• Time: 10:30am - 11:30am
• Location: Galois, Inc. 421 SW 6th Ave. Suite 300; Portland, OR 97204

For details (including an abstract and speaker bio), please see our blog post: http://www.galois.com/blog/2009/10/06/huffman-universal/

An RSVP is not required; but feel free to drop a line to [email protected] if you've any questions or comments.

Levent Erkok

The next talk in the Galois Tech Seminar series:

• Date: Tuesday, October 20th, 2009
• Title: Writing Linux Kernel Modules with Haskell
• Speaker: Thomas DuBuisson
• Time: 10:30am - 11:30am
• Location: Galois, Inc. 421 SW 6th Ave. Suite 300; Portland, OR 97204

For details (including an abstract and speaker bio), please see our blog post: http://www.galois.com/blog/2009/10/13/haskellkernelmodules/

An RSVP is not required; but feel free to drop a line to [email protected] if you've any questions or comments.

Levent Erkok

The next talk in the Galois Tech Seminar series:

• Date: Tuesday, October 27th, 2009
• Title: How to choose between a screwdriver and a drill
• Speaker: Tanya L. Crenshaw
• Time: 10:30am - 11:30am
• Location: Galois, Inc. 421 SW 6th Ave. Suite 300; Portland, OR 97204

For details (including an abstract and speaker bio), please see our blog post: http://www.galois.com/blog/2009/10/20/crenshaw-simplex/

An RSVP is not required; but feel free to drop a line to [email protected] if you've any questions or comments.

Levent Erkok

The next talk in the Galois Tech Seminar series:

• Date: Tuesday, November 3rd, 2009
• Title: Testing First-Order-Logic Axioms in AutoCert
• Speaker: Ki Yung Ahn
• Time: 10:30am - 11:30am
• Location: Galois, Inc. 421 SW 6th Ave. Suite 300; Portland, OR 97204

For details (including an abstract and speaker bio), please see our blog post: http://www.galois.com/blog/2009/10/28/ahn-autocert/

An RSVP is not required; but feel free to drop a line to [email protected] if you've any questions or comments.

Levent Erkok

[NB. This talk is on Friday, instead of the usual Tuesday slot.]

The next talk in the Galois Tech Seminar series:

• Date: Friday, November 13th, 2009
• Title: Hoare-Logic – fiddly details and small print
• Speaker: Rod Chapman
• Time: 10:30am - 11:30am
• Location: Galois, Inc. 421 SW 6th Ave. Suite 300; Portland, OR 97204

For details (including an abstract and speaker bio), please see our blog post: http://www.galois.com/blog/2009/11/04/chapman-hoare/

An RSVP is not required; but feel free to drop a line to [email protected] if you've any questions or comments.

Levent Erkok

Computers As We Don’t Know Them Christof Teuscher, PhD

Since the beginning of modern computer science some sixty years ago, we are building computers in pretty much the same way. Silicon transistor electronics serves as a physical device, the von Neumann architecture provides a computer design model, while the abstract Turing machine concept supports the theoretical foundations. However, in recent years, unimagined computing devices have seen the light because of advances in synthetic biology, nanotechnology, material science, and neuroscience. Many of these novel devices share the following characteristics: (1) they are made up from massive numbers of simple, stochastic components which (2) are embedded in 2D or 3D space in some disordered way. A grand challenge in consists in developing computing paradigms, design methodologies, formal frameworks, architectures, and tools that allow to reliably compute and efficiently solve problems with such devices. In this talk, I will outline my visionary and long-term research efforts to address the grand challenge of building, organizing, and programming future computing machines. First, I will review exemplary future and emerging computing devices and highlight the particular challenges that arise for performing computations them. I will then delineate potential solutions on how these challenges might be addressed. Self-assembled nano-scale cellular automata (CAs) and random boolean networks (RBNs) will serve as a simple showcase. I will also present the efforts underway to self-assemble massive-scale nanowire-based interconnect fabrics for spatial computers and what the challenges are in terms of computations and communication in such a non-classical system.

abcBridge: Functional interfaces for AIGs and SAT solving

Edward Z. Yang

SAT solvers are perhaps the most under-utilized high-tech tools that the modern software engineer has at their fingertips. An industrial strength SAT solver can solve most human generated NP-complete problems in time for lunch, and there are many, many practical problem domains which involve NP-complete problems. However, a major roadblock to using a SAT solver in your every day routine is translating your problem into SAT, and then running it on a highly optimized SAT solver, which is probably implemented in C or C++ and not your usual favorite programming language.

This talk is about the use, design and implementation of abcBridge, a set of Haskell bindings for ABC, a system for sequential synthesis and verification produced by the Berkeley Logic Synthesis and Verification Group. ABC looks at SAT solving from the following perspective: given two circuits of logic gates (ANDs and NOTs), are they equivalent? ABC is imperative C code: abcBridge provides a pure and type-safe interface for building and manipulating and-inverter graphs. We hope to release abcBridge soon as open source.

Presented by Priyank Kalla.

Applications in Cryptography require multiplication and exponentiation operations to be performed over Galois fields GF(2^k). Therefore, there has been quite an interest in the hardware design and optimization of such multipliers. This has led to impressive advancements in this area — such as the use of composite field decomposition techniques, use of Montgomery multiplication, among others.

My research group has recently begun investigations in the verification of such Galois Field multipliers. Unfortunately, the word-length (k) in such multipliers can be very large: typically, k = 256. Due to such large word-lengths, verification techniques based on decision diagrams, SAT and contemporary SMT solvers are infeasible. We are exploring the use of Computer Algebra techniques, mainly Groebner bases theory, to tackle this problem. In this talk, we will see why Groebner bases techniques look promising, while at the same time also studying the challanges that have to be overcome.

presenter: David Spivak

About five months ago I gave a talk here at Galois called “Databases are categories.” The basic idea was that a database schema can be represented as a category C and its states can be represented as functors C–>Set. In this talk I’ll refine that notion a bit, explaining that schemas are better represented as sketches. I’ll also show how, within this model one can: deal with incomplete data; incorporate typing and calculated fields; and perform queries, define views, and migrate data between disparate schemas. That is, I’ll try to show that the categorical approach handles everything one might hope it would. Finally, I’ll discuss a linguistic version of categories, called “ologs,” and show how they may help to democratize information storage.

Presented by Lee Pike.

We address the problem of runtime monitoring for hard real-time programs—a domain in which correctness is critical yet has largely been overlooked in the runtime monitoring community. We describe the challenges to runtime monitoring for this domain as well as an approach to satisfy the challenges. The core of our approach is a language and compiler called Copilot. Copilot is a stream-based dataflow language that generates small constant-time and constant-space C programs, implementing embedded monitors. Copilot also generates its own scheduler, obviating the need for an underlying real-time operating system. This talk will include fun pictures and videos.

speaker: Alwyn Goodloe

Critical cyber-physical systems, such as avionics, typically have one or more components that control the behavior of dynamical physical systems. The design of such control systems is well understood with mature and sophisticated foundations, but control engineers typically only work on Matlab/Simulink models, ignoring the implementation all together. I will speak about an ongoing collaboration with Prof. Eric Feron of Georgia Tech aimed at narrowing this gap. I will briefly describe the design of a Matlab to C translator being written in Haskell and verified using the Frama-C tool and the Prototype Verification System (PVS). In addition, I will give a survey of our efforts in enhancing PVS’ capabilities in this area by building a Linear Algebra library targeted at the math used by control engineers.

Presented by Brian Ford

Ruby is a highly dynamic, strongly-typed programming language created by Yukihiro Matsumoto in 1993 and first released in 1995. It borrows from Smalltalk, Lisp, and Perl. Ruby has single inheritance, mixins, and syntax features like omission of parentheses that make it well-suited for embedded domain-specific languages. Ruby was popularized by the Ruby on Rails web development framework.

The Rubinius project began as an implementation of the Ruby programming language roughly following the design of the Smalltalk-80 virtual machine described in the Blue book (“Smalltalk-80: the language and its implementation” by Adele Goldberg and David Robson). We have extended the initial implementation based on modern research in virtual machines, garbage collectors, and just-in-time (JIT) compilers. Rubinius currently features a stack-oriented opcode virtual machine, generational garbage collector, and LLVM-based JIT compiler. Most of the Ruby core library and the bytecode compiler are written in Ruby.

We will examine the main features of Rubinius and take a deeper dive into some aspects of the virtual machine and JIT compiler. We will also look at possible future work to address memory load, startup, and suitability for using Rubinius in Android phones. If there is time and interest, we will discuss implementing programming languages besides Ruby on Rubinius.

Presented by Brian Ford

Ruby is a highly dynamic, strongly-typed programming language created by Yukihiro Matsumoto in 1993 and first released in 1995. It borrows from Smalltalk, Lisp, and Perl. Ruby has single inheritance, mixins, and syntax features like omission of parentheses that make it well-suited for embedded domain-specific languages. Ruby was popularized by the Ruby on Rails web development framework.

The Rubinius project began as an implementation of the Ruby programming language roughly following the design of the Smalltalk-80 virtual machine described in the Blue book (“Smalltalk-80: the language and its implementation” by Adele Goldberg and David Robson). We have extended the initial implementation based on modern research in virtual machines, garbage collectors, and just-in-time (JIT) compilers. Rubinius currently features a stack-oriented opcode virtual machine, generational garbage collector, and LLVM-based JIT compiler. Most of the Ruby core library and the bytecode compiler are written in Ruby.

We will examine the main features of Rubinius and take a deeper dive into some aspects of the virtual machine and JIT compiler. We will also look at possible future work to address memory load, startup, and suitability for using Rubinius in Android phones. If there is time and interest, we will discuss implementing programming languages besides Ruby on Rubinius.

Presented by Rebekah Leslie.

The existing implementation of DDT uses a depth-first search algorithm to drive the exploration of new paths for testing. This algorithm provides full coverage of the program under test, but is limited by the fact that the number of paths increases exponentially with the size of the program. By employing the control-flow graph information of the program under test, we can direct the testing process towards program paths that contain unvisited points and therefore obtain full branch coverage in a smaller number of tests than would be required by the original depth-first search algorithm. We will present two uses of control-flow graph information in DDT. The first use is a refinement of depth-first search where control-flow graph information is used to prune the search space to eliminate unnecessary tests. The second use is in the context of a prioritized work-queue that forms the basis for a variety of sophisticated search algorithms that exploit different heuristics.

Presented by Aaron Tomb.

Many tools exist to automate the search for defects in software source code. However, many of these tools have not been widely applied, partly because they tend to work least well in the most common case: on large software systems that have only partial specifications describing correct behavior --- often a collection of independent assertions sprinkled throughout the program.

Recent research has suggested that a large class of software bugs fall into the category of inconsistencies, or cases where two pieces of program code make incompatible assumptions. Existing approaches to inconsistency detection have used intentionally unsound techniques aimed at bug-finding rather than verification. In this dissertation, we describe an inconsistency detection analysis that subsumes previous work and is instead based on the foundation of the weakest precondition calculus.

We have applied our analysis to a large body of widely-used open-source software, and found a number of bugs.

Presented by Simon Winwood.

In 2009 the NICTA L4.verified project completed the machine-checked correctness proof of the seL4 microkernel. The natural next step is then to use this verified kernel to construct verified systems.

In this talk I give an overview of the ongoing work into systems verification in the Trustworthy Embedded Systems project. In particular, I will focus on the use of access control results to reason about the properties of systems in the presence of large untrusted components, such as a Linux kernel.

Presented by Grant Passmore.

In automated deduction, strategy is a vital ingredient in effective proof search. Strategy comes in many forms, but the key is this: user-specifiable adaptations of general reasoning mechanisms reduce the search space by tailoring its exploration to a particular class of problems. In fully automatic theorem provers, this may happen through formula weights, term orders and quantifier triggers. In interactive proof assistants, one may build strategies by programming tactics and carefully crafting systems of rewrite rules. Given that automated deduction often takes place over undecidable theories, the recognition of a need for strategy is natural and happened early in the field. In computer algebra, the situation is rather different.

In computer algebra, the theories one works over are often decidable but inherently infeasible. For instance, the theory of real closed fields (i.e., nonlinear real arithmetic) is decidable, but any full quantifier elimination algorithm for it is guaranteed to have worst-case doubly exponential time complexity. The situation is similar with algebraically closed fields (e.g., through Groebner bases), and many others. Usually, decision procedures arising from computer algebra admit little means for a user to control them. But, when it comes to practical applications, is an infeasible theory really so different from an undecidable one?

The Strategy Challenge in Computer Algebra is this: To build theoretical and practical tools allowing users to exert strategic control over the execution of core computer algebra algorithms. In this way, such algorithms may be tailored to specific problem domains. For formal verification efforts, the focus of this challenge upon decision procedures is especially relevant. In this talk, we will motivate this challenge and present two examples from our dissertation: (i) the theory of Abstract Groebner Bases and its use in developing new Groebner basis algorithms tailored to the needs of SMT solvers (joint with Leo de Moura), and (ii) the theory of Abstract Cylindrical Algebraic Decomposition and a family of real quantifier elimination algorithms tailored to the structure of nonlinear real arithmetic problems arising in specific formal verification tool-chains. The former forms the foundation of nonlinear arithmetic in the SMT solver Z3, and the latter forms the basis of our tool RAHD (Real Algebra in High Dimensions).

Presented by Johan Tibell.

The most commonly used map (dictionary) data type in Haskell is implemented using a size balanced tree. While size balanced trees provide good asymptotic performance, their real world performance is not stellar, especially when used with keys which are expensive to compare, such as strings.

In this talk we will look at two different map implementations that use hashing to achieve better real world performance. The implementations have different performance characteristics: one provides very fast look-ups while the other trades better insert performance for somewhat slower look-ups. I will describe the design of these data structures and show some early benchmark results.

Presented by Rachel Lanigan.

Engineers Without Borders USA is a fast-growing national non-profit impacting developing communities around the world. EWB provides an opportunity for engineering students and professionals to use their skills to develop sustainable, appropriate technologies for specific applications, to help meet the basic needs of people. Our programs typically start with a focus on providing water and sanitation, but often move into other areas depending on the needs of the people. There is a role for everyone at EWB, from engineers to public health professionals. Rachel will give a background on EWB, our local chapter, and how to get involved.

Presented by Philip Weaver.

Janrain offers user management services that include single sign-on, social login, and profile storage. We have recently begun using Haskell extensively to implement our products, and would like to share what the experience has been like.

In this talk we will give a technical demonstration of Capture, whose backend is written in Haskell, discuss some of the implementation details of Capture, and look at some of the joys and pitfalls that we experienced.

Presented by Joe Hurd.

Interactive theorem proving is tackling ever larger formalization and verification projects, and there is a critical need for theory engineering techniques to support these efforts. One such technique is cross-prover package management, which has the potential to simplify the development of logical theories and effectively share theories between different theorem prover implementations. The OpenTheory project has developed standards for packaging theories of the higher order logic implemented by the HOL family of theorem provers. What is currently missing is a standard theory library that can serve as a published contract of interoperability and contain proofs of basic properties that would otherwise appear in many theory packages. This talk will present a standard theory library for higher order logic represented as an OpenTheory package. We identify the core theory set of the HOL family of theorem provers, and describe the process of instrumenting the HOL Light theorem prover to extract a standardized version of its core theory development. We profile the axioms and theorems of our standard theory library and investigate the performance cost of separating the standard theory library into coherent hierarchical theory packages.

Presented by Jim Snow.

RNA Networks is a software company focused on providing the next generation storage cache solution that addresses performance deficiencies and the rising cost of storage for virtual environments. Our software solution utilizes compute resources (DRAM and flash) as a distributed clustered cache moving 'active' data off of the storage tier and into the compute tier translating to significant performance gains with no additional investment in hardware resources. RNA's MVX technology is based on a distributed shared memory core that leverages RDMA fabrics and allows for a unified and flexible namespace that can scale proportionally to meet any performance or capacity need.

In this presentation we'll discuss the core architecture and how this can be leveraged to both reduce the cost of high end storage and meet high performance storage objectives.

Presented by Chad Scherrer.

Sampling from a large discrete distribution is a common problem in statistics. In this talk, we'll consider a real-world situation where the properties of the distribution cause common approaches to break down, and we'll arrive at a Haskell-based solution that fixes the problem.

Presented by Nicholas Begley, Dave Dung Anh, James Heilinger, Alec Rasmussen, and Mark Theuson.

It's a bird! It's a plane! No, it's an open-source autonomous quad-copter. In collaboration with the Portland State University Electrical and Computer Engineering Dept., Galois mentored a Spring semester Senior Capstone Project to build an ArduCopter. The ArduCopter is based on the Arduino open-source hardware platform, and includes infrared sensors (collision avoidance), sonar and barometer (altitude hold), GPS (location), magnetometer (direction), and gyro (stabilization). This talk will include a description of the ArduCopter and it's operation, including the trials and tribulations of building and testing one. Of course, the talk will include cool videos.

Presented by Temesghen Kahsai.

We give an overview of a parallel k-induction-based model checking architecture for verifying safety properties of synchronous systems. The architecture, which is strictly message-based, is designed to minimize synchronization delays and easily accommodate the incorporation of incremental invariant generators to enhance basic k-induction. A first level of parallelism is introduced in the k-induction procedure itself by executing the base and the inductive steps concurrently. A second level of parallelism allows the addition of one or more independent processes that incrementally generate invariants for the system being verified. The invariants are fed to the k-induction loop as soon as they are produced and used to strengthen the induction hypothesis.

This architecture allows the verification of multiple properties in an incremental fashion. Specifically, the outcome of a property -- valid or invalid -- is communicated to the user as soon as the result is known. Moreover, verified valid properties are added as invariants in the model checking procedure to aid the verification of the remaining properties.

We provide experimental evidence that this incremental and parallel architecture significantly speeds up the verification of safety properties. Additionally, due to the automatic invariant generation, it also considerably increases the number of provable safety properties.

Presented by Adam Foltzer.

Interpreters offer a convenient and intuitive way for programmers to reason about language behavior through denotational semantics. However in a setting like Coq, where all recursive functions must provably terminate, it is impossible to write interpreters for non-terminating languages. The standard alternative is to inductively define operational semantics, but this can yield proofs that are difficult to automate, particularly in the presence of changing language features.

This talk presents a combined approach, where an interpreter is used in combination with operational semantics to prove type preservation of a small functional language. To demonstrate the scalability of the Coq development, let expressions and a pair types will be added and preservation will be proved again with only one extra line of proof script.

This technique and development are adapted from Greg Morrisett's lectures at the 2011 Oregon Programming Languages Summer School, and are available at his web site.

Presented by Kristin Rozier

Formal behavioral specifications written early in the system-design process and communicated across all design phases have been shown to increase the efficiency, consistency, and quality of the system under development. To prevent introducing design or verification errors, it is crucial to test specifications for satisfiability. Our focus here is on specifications expressed in linear temporal logic (LTL).

We introduce a novel encoding of symbolic transition-based Buchi automata and a novel, ``sloppy,'' transition encoding, both of which result in improved scalability. We also define novel BDD variable orders based on tree decomposition of formula parse trees. We describe and extensively test a new multi-encoding approach utilizing these novel encoding techniques to create 30 encoding variations. We show that our novel encodings translate to significant, sometimes exponential, improvement over the current standard encoding for symbolic LTL satisfiability checking.

Details can be found here: http://ti.arc.nasa.gov/profile/kyrozier/.

Presented by Sebastian Niller and Nis N. Wegmann

1

title: Translation of Functionally Embedded Domain-specific Languages With Static Type Preservation by using Witnesses

abstract: Static type preservation automatically guarantees type-correctness of an embedded domain-specific language (eDSL) by tying its type system to that of the host-language. Not only does this obviate the need for a custom type checker, it also preserves type-correctness during code transformations and optimizations, and simplifies and increases the efficiency of interpreters. When implementing a translator from a source DSL with type preservation to a target DSL, the commonly chosen approach requires the incorporation of extensions in the source DSL specific to the target DSL, which, in cases where multiple back-ends are required, obfuscates the source DSL and decreases the overall modularity. We show that by using witnesses, a technique which facilitates the construction of type-level proofs, we can effectively cope with this issue and implement translators without extending the source DSL.

We have applied our approach on Copilot, a Haskell-embedded domain specific language for runtime monitoring of hard real-time distributed systems, and used it for implementing two back-ends targeting the Haskell-embedded languages Atom and SBV. Our approach restrains to the Haskell 2010 Standard except for existentially and universally quantified types.

2

title: From High-Level Languages to Monitoring Fault-Tolerant Hardware: Case-Studies of Runtime Verification Using Copilot

abstract: Failures of hard real-time systems can be caused by systematic faults in software and hardware, as well as by random hardware faults, and faults due to wear out of hardware components. Even if monitoring software is proven to comply to its specification, there is no guarantee that failing underlying hardware does not affect the monitors themselves. An application of distributed Copilot monitors to a redundant airspeed measurement system is presented. We show the use of monitors enables the system to withstand benign and Byzantine hardware and software faults.

The second part of the talk presents current work using Copilot to monitor the MAVLink protocol in flight of a sub-scale model of an Edge 540T aircraft.

Presented by Alexey Gotsman

Most major OS kernels today run on multiprocessor systems and are preemptive: it is possible for a process running in the kernel mode to get descheduled. Existing modular techniques for verifying concurrent code are not directly applicable in this setting: they rely on scheduling being implemented correctly, and in a preemptive kernel, the correctness of the scheduler is interdependent with the correctness of the code it schedules. This interdependency is even stronger in mainstream kernels, such as Linux, FreeBSD or XNU, where the scheduler and processes interact in complex ways. In this talk I will present the first logic that is able to decompose the verification of preemptive multiprocessor kernel code into verifying the scheduler and the rest of the kernel separately, even in the presence of complex interdependencies between the two components present in mainstream kernels. This is joint work with Hongseok Yang (University of Oxford, UK).

Presented by Kevin Butler

The complexity of modern operating systems makes securing them a challenging problem. However, changes in the computing model, such as the rise of cloud computing and smarter peripherals, have presented opportunities to reconsider system architectures, as we move from traditional "stove-pipe" computing to distributed systems. In particular, we can build trustworthy components that act to provide security in complex systems.

This talk discusses how new disk architectures may be exploited to aid the protection of systems by acting as policy decision and enforcement points. We prototype disks that enforce data immutability at the block level on critical system data, preventing malicious code from inserting itself into system configuration and boot files. We then examine how storage may be used to ensure the integrity state of hosts prior to allowing access to data, and how such a design improves the security of portable storage devices. Using continual measurements of system state, we show through formal reasoning that such a device enforces guarantees that data is read and written while the host is in a good state. Finally, we discuss some recent initiatives to assure the identity of the host and identify future directions for exploring the interface between storage and operating system security.

Presented by Dylan McNamee.

This talk is an introduction to the MILS (Multiple Independent Layers of Security) architecture, motivated by the challenge of enforcing various kinds of security policies. I'll describe the goals of policy enforcement, traditional means of implementing security enforcement mechanisms, and the emerging MILS architecture for enforcing policies with high assurance.

Presented by Eric Migicovsky.

Hardware is hard. At least that's what people always say. Building a hardware startup requires a broad base of technical knowledge, from electronics and manufacturing experience to aesthetic and interface design. But Eric Migicovsky chose to start a hardware company after graduating from engineering because he wanted to see something he designed become a physical reality.

inPulse is a $150 hackable Bluetooth smartwatch. It connects to your smartphone and displays notifications like incoming emails, calls, and calendar alerts right on your wrist. After launching an SDK, 3rd party developers have started to create apps for inPulse.

In his talk, Eric will share some honest stories and anecdotes from various stages of product development. He'll also talk about the costs, timeframes and failure modes of hardware startups.

Presented by Nate Foster.

The languages used to program networks today lack modern features. Programming them is a complicated task, and outages and infiltrations are frequent. We believe it is time to develop NETWORK PROGRAMMING LANGUAGES with the following essential features:

• High-level abstractions that give programmers direct control over the network, allowing them to specify what they want the network to do without worrying about how to implement it.

• Compositional constructs that facilitate modular reasoning about programs.

• Portability, allowing programs written for one platform to be used with different devices.

• Rigorous semantic foundations that precisely document the meaning of the language and provide a basis for building formal verification tools.

The Frenetic language addresses these challenges in the context of OpenFlow networks. It combines a streaming declarative query sub-language and a functional reactive sub-language that, together, provide many of the features listed above. Our implementation handles many low-level packet-processing details and keeps traffic in the "fast path" whenever possible.

Presented by David Lazar

Formal semantics is notoriously hard. The K semantic framework (http://k-framework.org/) is a system that makes the task of formally defining programming languages easy and practical. The primary goals of the K framework are modularity, expressivity, and executability. Adding a new language feature to a K definition does not require you to revisit and modify existing semantic rules. The K framework is able to concisely capture the semantics of non-determinism and concurrency. Each K definition automatically yields an interpreter for the language so that the definition can be tested for correctness. These features made it possible to develop a complete formal semantics of the C language in K. The first half of the talk will be an overview of the K semantic framework. We'll discuss the merits of the framework using the K definition of a complex toy language as a guiding example. The second half of the talk will focus on a work-in-progress formalization of Haskell 98 in K. We'll look at the challenges of formalizing Haskell and the applications of this work.

Presented by Borzoo Bonakdarpour.

Design and implementation of distributed systems often involve many subtleties due to their complex structure, non-determinism, and low atomicity as well as occurrence of unanticipated physical events such as faults. Thus, constructing correct distributed systems has always been a challenge and often subject to serious errors. We propose a method for generating distributed implementations from high-level component-based models that only employ simple synchronization primitives. The method is a sequence of three transformations preserving observational equivalence: (1) A transformation from a global state to a partial state model, (2) a transformation which replaces multi-party strong synchronization primitives in atomic components by point-to-point send/receive primitives based on asynchronous message passing, and (3) a final transformation to concrete distributed implementation based on platform and architecture. We study the properties of different transformations, in particular, performance criteria such as degree of parallelism and overhead for coordination.

The second part of the talk will focus on an automated technique for optimal instrumentation of multi-threaded programs for debugging and testing of concurrent data structures. We define a notion of observability that enables debuggers to trace back and locate errors through data-flow instrumentation. Observability in a concurrent program enables a debugger to extract the value of a set of desired variables through instrumenting another (possibly smaller) set of variables. We formulate an optimization problem that aims at minimizing the size of the latter set. Our experimental results on popular concurrent data structures (e.g., linked lists and red-black trees) show significant performance improvement in optimally-instrumented programs using our method as compared to ad-hoc over-instrumented programs.

Presented by Julien Schmaltz.

Communication fabrics constitute an important challenge for the design and verification of multicore architectures. To enable their formal analysis, micro-architectural models have been proposed as an efficient abstraction capturing the high-level structure of designs. Micro-architectural models also include a representation of the protocols using the communication fabrics. This combination of different aspects in a single model is crucial for deadlock verification. Deadlocks emerge or are prevented in this combination: a system with a deadlock-free communication network combined with a deadlock-free protocol may have deadlocks or a system with a network with deadlocks combined with a deadlock-free protocol may be deadlock-free. This combination also makes the verification problem more complicated. We will present an algorithm for efficient deadlock verification in micro-architectural models. We will discuss the limitations of this approach and point to future research direction. An important future application of our methodology is the verification of cache coherency at the level of micro-architectures.

Presented by Alan Mishchenko.

Last spring, in March 2010, Aaron Bradley published the first truly new bit-level symbolic model checking algorithm since Ken McMillan’s interpolation based model checking procedure introduced in 2003. Our experience with the algorithm suggests that it is stronger than interpolation on industrial problems, and that it is an important algorithm to study further. In this paper, we present a simplified and faster implementation of Bradley’s procedure, and discuss our successful and unsuccessful attempts to improve it.

Presented by Charles Parker

A basic problem in computer science is binary classification, in which an algorithm applies a binary label to data based on the presence or absence of some phenomenon. Problems of this type abound in areas as diverse as computational biology, multimedia indexing, and anomaly detection. Evaluating the performance of a binary labeling algorithm is itself a complex task, often based on a domain-dependent notion of the relative cost of "false positives" versus "false negatives". As these costs are often not available to researchers or engineers, a number of methods are used to provide a cost-independent analysis of performance. In this talk, I will examine a number of these methods both theoretically and experimentally. The presented results suggest a set of best practices for evaluating binary classification algorithms, while questioning whether a cost-independent analysis is even possible.

Presented by Chris Andrew, Kayla Seliner, Mark Craig, and Trang Nguyen.

On October 7, 2008, the flight control system of Qantas flight 72 malfunctioned without warning. The failure caused the aircraft to violently pitch down with an acceleration of -0.8g, pitching passengers and crew into the roof of the cabin resulting in many injuries. In the investigation that followed, the malfunction was attributed to a software problem in the Air Data Inertial Reference Unit. These units are utilized on all modern passenger jets, but are proprietary devices not open to public scrutiny.

This capstone project develops an open source Air Data Inertial Reference Unit using four redundant Arduino boards each with a microcontroller, 3D gyroscope and accelerometer. Faults are injected into the system through software and outputs are monitored over serial ports allowing the user to test effectiveness of fault-tolerant algorithms to mask fail silent and byzantine faults in the sensors. Failures in ADIRU systems are usually complex in nature and arise under very anomalous circumstances suggesting that fault-tolerant system design could benefit from the diverse testing and evaluation that can occur in an open source community. This project demonstrates the low entry-cost to building a fault-tolerant system for open-source design and experimentation.

Presented by Sergio Antoy from Portland State University.

In this talk, I will introduce narrowing, the characterizing feature of functional logic programming, from the programmer's viepoint. Narrowing promotes non-determinism and it enables computing with incomplete or unknown information. After a short and informal presentation of Curry, the leading functional logic language, I will discuss a few examples showing that narrowing and its associated non-determinism support programming at a very high level of abstraction.

Presented by Iulian Neamtiu.

The relative novelty and rapid evolution pace of the Android ecosystem (platform, vendor-installed apps and third-party apps) means both the platform and apps receive little scrutiny. Hence there is a need for tools that assess, monitor and verify all components of the Android ecosystem. This lack of tools and scrutiny is particularly problematic when combined with the open nature of Google Play, the main app distribution channel.

In the first part of this talk we will focus on multi-layer profiling of Android apps using ProfileDroid, a tool and framework we developed at UC Riverside. ProfileDroid is useful for a variety of Android app analyses, from performance to usability to security. ProfileDroid monitors and correlates the behavior of an app at four layers: (a) static, or app specification (b) user interaction, (c) operating system, and (d) network layer. Using ProfileDroid on 27 free and paid Android apps, we have revealed: (a) discrepancies between the app specification and app execution, (b) free versions of apps could end up costing more than their paid counterparts, due to an order of magnitude increase in traffic, (c) most network traffic is not encrypted, (d) apps communicate with many more sources than users might expect.

In the second part of the talk we will present results from our long-term permission evolution study of the Android ecosystem---platform and 237 apps---over three years. We found that the platform has increased the number of dangerous permissions and does not move towards finer-grained permissions, and that app developers do not follow the principle of least privilege. We will also briefly discuss our efforts with static information flow tracking for Android apps, as well as building a log-and-replay system for Android.

Presented by Larry Diehl.

Many advanced branches of mathematics involve structures that abstract over well known specific instances, e.g. abstract algebraic structures, equivalence relations, various orders, category theoretic structures, etc. In typed functional programming (e.g. with type classes in Haskell), encoding such structures amounts to enforcing the definition of elements and operations for a particular structure instance on one hand, and being able to use said elements and operations in generic definitions on the other hand. With Dependently Typed Programming (DTP) we can go one step further and define propositions/properties for abstract structures, and subsequently require proofs in particular instances.

This talk will tell the story of how examples of particular instances inspire an abstract definition (including its propositional properties), how to then instantiate the original concrete examples in the new abstract definition, and finally create further abstract definitions that depend on previously defined ones. Emphasis will be given on how easily concrete proofs can be used as evidence for abstract propositions, and how proofs about abstract structures parameterized by other abstract structures may reuse their proofs (similar to the more common concept of reusing operations in subsequent abstract definitions). The talk will use Agda as its demonstration language, but proofs will mostly be in the form of equational reasoning that should look familiar to the non-expert.

Presented by Brian Huffman.

We present techniques for reasoning about constructor classes that (like the monad class) fix polymorphic operations and assert polymorphic axioms. We do not require a logic with first-class type constructors, first-class polymorphism, or type quantification; instead, we rely on a domain-theoretic model of the type system in a universal domain to provide these features. These ideas are implemented in the Tycon library for the Isabelle theorem prover, which builds on the HOLCF library of domain theory. The Tycon library provides various axiomatic type constructor classes, including functors and monads. It also provides automation for instantiating those classes, and for defining further subclasses. We use the Tycon library to formalize three Haskell monad transformers: the error transformer, the writer transformer, and the resumption transformer. The error and writer transformers do not universally preserve the monad laws; however, we establish datatype invariants for each, showing that they are valid monads when viewed as abstract datatypes.

Presented by Matthew Fernandez.

In safety- and security-critical environments software failures that are acceptable in other contexts may have expensive or even life-threatening consequences. Formal verification has the potential to provide high assurance for this software, but is regarded as being prohibitively expensive. Although significant advances have been made in this area, verification of larger systems still remains impractical. Component-based development has the potential to lower the cost of system-wide verification, bringing correctness proofs of these large scale systems within reach. This talk will discuss my work that aims to provide a component-based development environment for building systems with high assurance requirements. By providing a formal model of the platform with proven correctness properties that hold at the level of an abstract model right down to the implementation, I hope to reduce the cost of full system verification by allowing reasoning about system components in isolation.

COPIOUS is a user-centered digital experience agency. We build digital products with the user at heart and technology in our bones. We recently moved to a new office and now have a large space to host our TechTalks.

About TechTalks:

COPIOUSLabs TechTalks series meets every other Friday at 1pm at the COPIOUS offices. Our talks span artificial intelligence, new programming languages and techniques, computational linguistics, geographic data processing, systems and software architecture, augmented reality, network security, and more as proposed to the Copious engineering team.

About this talk:

Speaker: John Jessee

As new programming languages emerge, Microsoft's flagship programming language has been evolving to keep up. See how C# and the .NET Framework have incorporated new features such as functional programming, non-blocking code, language integrated queries, and more. This talk compares C# and the .NET Framework to the languages found in the book, Seven Languages in Seven Weeks, and in particular COPIOUS' most "native" tongue, Ruby.

All are welcome to attend. If you have a talk that you'd like to suggest presenting, please email it to [email protected] along with a brief outline of what you'd like to cover.

Presented by Daniel Matichuk.

Formal verification can provide a high degree of assurance for critical software, but can come at the cost of large artefacts that must be maintained alongside it. When using an interactive theorem prover, these artefacts take the form of large, complex proofs where the ability to reuse and maintain them becomes paramount. I will present my work on a function annotation logic, which is an extension to Hoare logic that allows reasoning on intermediate program states to be easily reused. Program functions are annotated with properties as a side-condition of existing proofs. These annotations can reduce the proof burden substantially when subsequent program properties need to be shown. Implemented in Isabelle, it is shown to be practically useful by greatly simplifying cases where existing proofs contained largely duplicated reasoning.

COPIOUS is a user-centered digital experience agency. We build digital products with the user at heart and technology in our bones. We recently moved to a new office and now have a large space to host our TechTalks.

About TechTalks:

COPIOUSLabs TechTalks series meets every other Friday at 1pm at the COPIOUS offices. Our talks span artificial intelligence, new programming languages and techniques, computational linguistics, geographic data processing, systems and software architecture, augmented reality, network security, and more as proposed to the Copious engineering team.

About this talk:

Speaker: Brian Shirai

Writing your own programming language can be very different from writing a program in an existing language. However, it is less intimidating than many people assume. This Friday, Brian Shirai from Engine Yard will present a talk about features of the Rubinius dynamic language platform that make writing your own programming language simple and fun.

All are welcome to attend. If you have a talk that you'd like to suggest presenting, please email it to [email protected] along with a brief outline of what you'd like to cover.

Presented by Brian Huffman.

A polymorphic function may be instantiated at many different types; if the function is parametrically polymorphic, then all of its instances must behave uniformly. Reynolds' parametricity theorem expresses this precisely, in terms of binary relations derived from types. One application of the parametricity theorem is to derive Wadler-style "free theorems" about a polymorphic function from its type; e.g. rev :: [a] -> [a] must satisfy map f (rev xs) = rev (map f xs).

In this talk, I will show how to apply many of the ideas behind parametricity and free theorems in a new setting: formal reasoning about quotient types. Using types-as-binary-relations, we can automatically prove that corresponding propositions about quotient types and their representation types are logically equivalent. This design is implemented as the Transfer package in the Isabelle theorem prover, where it is used to automate many proofs about quotient types.

Presented by Erlend Hamberg.

An important problem in genetics is phylogenetic inference: Coming up with good hypotheses for the evolutionary relationship between species – usually represented as a “family tree”. As the amount of molecular data (e.g. DNA sequences) quickly grows, efficient algorithms become increasingly important to analyze this data. A maximum-likelihood approach with models for nucleotide evolution allows us to use all the sequence data, but is a computationally expensive approach. The number of possible trees also grows rapidly as we include more species. It is therefore necessary to use heuristic search methods to find good hypotheses for the “true” tree. Evolutionary algorithms (EA) is a class of such search/optimization algorithms that has been shown to perform well in other areas where the search space is large and irregular. I will explain my approach and my findings from using an evolutionary algorithm for inferring phylogenies from molecular data.

Presented by Andrew Farmer.

The importance of reasoning about and refactoring programs is a central tenet of functional programming. Yet our compilers and development toolchains only provide rudimentary support for these tasks, leaving the programmer to do them by hand. This talk introduces HERMIT, a toolkit enabling informal but systematic transformation of Haskell programs from inside the Glasgow Haskell Compiler's optimization pipeline. With HERMIT, users can experiment with optimizations and equational reasoning, while the tedious heavy lifting of performing the actual transformations is done for them. The talk will explore design choices in HERMIT, demonstrate its use on examples, and seek input for further development and case studies.

Presented by Joe FitzPatrick.

Generally, there is a very low barrier to entry when it comes to software or network-based attacks due to the fact that actual costs are minimal and most resources are readily available. This does mean that it's generally much easier to attack the software of a system than the hardware, but unfortunately that also leads to overconfidence in, as well as misplaced trust in hardware.

There is a clear 'hierarchy of attacks' in the hardware world. There are costs, often significant, involved in acquiring your hardware 'target' which might be damaged or destroyed in the process. There are a number of useful tools that cost anywhere from a few dollars to a few million dollars. I'll give a couple examples of what's possible within budgets of $100, $10,000, and $1,000,000. I'll point out how many capabilities are much more accessible than most assume, and how vulnerable to sub-$100 attacks most of our 'secure' hardware really is.

Five students in PSU’s Electrical and Computer Engineering Senior Capstone sequence want to show you what they’ve created: an inexpensive computer vision system for a quadcopter running on a Raspberry Pi board. One might be surprised how simple it is to code a decent object tracking algorithm using open-source software, and how difficult it is to keep a quadcopter from crashing into the wall in the debug stage. This talk should appeal to the RC hobbyist, the embedded systems programmer, and anyone interested in the art of computer vision. The presentation will include video footage of what these students have accomplished and how they pulled it off.

Presented by Gerwin Klein and Thomas Sewell.

This talk introduces two new facets that have recently been added to the seL4 formal verification story: a proof the kernel does not leak information between domains, and a proof that the compiled binary matches the expected semantics of the C source code.

The first part of the talk presents a new non-interference theorem for seL4, which builds on the earlier function correctness verification. The theorem shows how seL4 can be configured as a static separation kernel with dynamic kernel services within each domain.

The binary proof addresses the compiler-correctness assumption of the earlier seL4 proofs by connecting the compiled binary to the refinement chain, thus showing that the seL4 binary used in practice has all of the properties that have been shown of its models. We use the Cambridge ARM model and Magnus Myreen's certifying decompiler, together with a custom correspondence finder for assembly-like programs powered by modern SMT solvers. We cover the previously-verified parts of seL4 as compiled by gcc (4.5.1) at optimisation level 1.

Presented by Neil Sculthorpe.

In Haskell, there are many data types that would form monads were it not for the presence of type-class constraints on the operations on that data type. This is a frustrating problem in practice, because there is a considerable amount of support and infrastructure for monads that these data types cannot use. This talk will demonstrate that a monadic computation can be restructured into a normal form such that the standard monad class can be used. The technique is not specific to monads --- it can also be applied to other structures, such as applicative functors. One significant use case for this technique is Domain Specific Languages, where it is often desirable to compile a deep embedding of a computation to some other language, which requires restricting the types that can appear in that computation.

Presented by Pat Hickey.

At Galois, we're building critical flight control software using new software methods for embedded systems programming. We will show how we used new domain-specific languages which permit low-level hardware manipulation while still providing guarantees of type and memory safety. The flagship application for these new languages is called SMACCMPilot, a clean slate design of quadcopter flight control software built on open-source hardware. This talk will introduce our new software methods and show how we built SMACCMPilot to be high assurance without sacrificing programmer productivity.

Presented by Jesse Hallett.

Take control of your hardware by installing an open build of Android. Get root access and extend the life of your device. Learn about what is involved in installing a third-party OS on your phone or tablet.

Academic papers often describe typed calculi, but it is rare to find one in a production compiler. Indeed, I think the Glasgow Haskell Compiler (GHC) may be the only production compiler in the world that really has a remorselessly statically-typed intermediate language, informally called "Core", or (when writing academic papers) the more respectable-sounding "System FC".

As real compilers go, GHC's Core language is tiny: it is a slight extension of System F, with letrec, data types, and case expressions. Yet all of Haskell (now a bit of a monster) gets translated into it. In the last few years we have added one new feature to Core, namely typed (but erasable) coercions that witness type equalities, which turn Core into a particular kind of proof-carrying code. This single addition has opened the door to a range of source-language extensions, such as GADTs and type families.

In this talk I'll describe Core, and how it has affected GHC's development over the last two decades, concentrating particularly on recent developments, coercions, evidence, and type families. To test your mettle I hope to end up with the problem we are currently wrestling with: proving consistency of a non-terminating rewrite system with non-left-linear rules.

Presented by Alex Groce.

One of the most effective ways to test complex language implementations, file systems, and other critical systems software is random test generation. This talk will cover a number of recent results that show how---despite the importance of hand-tooled random test generators for complex testing targets--- there are methods that can be easily applied in almost any setting to greatly improve the effectiveness of random testing. Surprisingly, giving up on potentially finding any bug with every test makes it possible to find more bugs over all. The practical problem of finding distinct bugs in a large set of randomly generated tests, where the frequency of some bugs may be orders of magnitude higher than other bugs, is also open to non ad-hoc methods.

Small unmanned aircraft---more often called drones---are set to make a big impact on agriculture. You already know about military drones operating overseas, and perhaps you've even seen recreational drones starring in youtube videos, but as the FAA begins permitting commercial use of unmanned aircraft in 2015, you'll see drones replacing all sorts of roles that used to require a manned aircraft, and taking on new roles made possible by their low cost, versatility, and safety.

Chris Anderson will speak about the upcoming role of drones in agriculture, a field Chris says "is a big data problem without the big data." Chris will describe how farmers can will drones to curb plant disease, conserve water, and reduce pesticide and fertilizer use. He'll discuss the challenges ahead to integrate air vehicle systems with sensors, specialized cameras, and data processing.

Please join the PDX Tech Community at NIKE for the next tech talks! The event will feature two speakers, networking time, and plenty of snacks and drinks.

Building a System for Machine and Event-Oriented Data Eric Sammer, Rocana

Facebook Platform Integrity: Fighting Social Spam Jonathan Gross, Facebook

Learn more about the talks and RSVP at: http://niketechtalks-june2015.splashthat.com

**Please note that the event will start at 4:00pm, 1/2 hour later than prior events.

Clear your calendar! Nike Consumer Digital Tech is hosting tech talks for the PDX tech community on August 13th. We're bringing two great speakers to the Nike campus and there will be time to network and enjoy snacks and drinks.

Real-Time Anomaly Detection Gwen Shapira / System Architect, Confluent / @gwenshap

FLP Off Your Thinking CAP Nathan Aschbacher / Lead System Architect, Visa / @n_aschbacher

RSVP and learn more at: https://niketechtalks-august2015.splashthat.com!

Join us for a tech talk at The Tech Academy. Our guest speaker is Michael Kaiser-Nyman, founder of Epicodus!

Code Fellows invites online learners of all stripes to Code Oregon Labs. We'll kick off this month's lab with a 30 minute demo on how to build a responsive website -- a site that adapts to user devices (mobile, tablet, desktop).

Jana Uhrich, developer at WebMD Health Services will do a 30 minute demo, followed by the usual open lab with volunteer tutors on hand to help you with whatever you're working on.

The 30 min. talk/demo will focus on HTML, CSS, & JavaScript. Tutors are knowledgeable on these and other stacks.

Together with Code Oregon and volunteers from the community, Code Fellows provides tutors at a 6:1 ratio -- and pizza for the hungry!

Join Nike Digital for the Nike Tech Talks on June 6th! Riva-Melissa Tez, Managing Partner at Permutation Ventures and a 2017 recipient of the Forbes 30 under 30 for Finance, will be joining us to give a talk titled, What You Actually Need to Know about the Artificial Intelligence Revolution. Enjoy some food and drinks while networking before and after the talk!

About the Talk: Artificial intelligence is everywhere. How will it affect us as people, companies and as a species? This talk will explore the current progress of AI, where it came from and where it's going.

About Riva: Riva is a managing partner at Permutation Ventures, an early stage VC fund focused on applied machine learning companies. She has held teaching positions at the DAB and HTW Business Schools and has guest-lectured at Oxford, Birkbeck, and Stanford. Riva writes about artificial intelligence, finance, and philosophy and represented AI in a 2016 Microsoft campaign for The Economist and was a 2017 recipient of Forbes 30 under 30 for finance.

(Please RSVP: https://www.eventbrite.com/e/women-talking-tech-series-pdx-tickets-38082154750)

So many of us are building really cool shit at work and in the community - let's share, recognize and applaud our badassery. Through this WTT series, we aim to perpetuate the technical learning and teaching component within our industry.

Partnering with local WIT communities we'll meet monthly for a lightning talk + keynote, followed by Q&A. Oh, and food/drink. Curated for a technical audience compromised of but not limited to women, transgender and non binary friends. We'll start promptly at 5:15 and end by 6:30, we welcome kiddos too.

October Lineup

Lightning Talk: TBD

Keynote: Liz Fong-Jones @lizthegrey. Site Reliability Engineering @ Google.

Liz is a Senior Site Reliability Engineer at Google and manages a team of SREs responsible for Google's storage systems. She lives with her wife, metamour, and two Samoyeds in Brooklyn. In her spare time, she plays classical piano, leads an EVE Online alliance, and advocates for transgender rights.

Questions/want to chat/interested in speaking at our 11/7 event? [email protected]

Wanna work in tech? Are you wondering what kinds of jobs are available, whether your resume will stand out, and how to land your dream job? Join Airbnb, Adidas, eBay, Mathys & Potestio, Thinkful and Say Media as they discuss the ins and outs of the hiring process. Come for the panel, stay for the cocktails! If you work in tech already...bring a friend looking to break into the industry and make new friends at our reception afterwards!

Out in Tech unites the LGBTQ+ tech community. We empower aspiring tech leaders to improve our world by showcasing accomplished speakers, producing timely and thought-provoking events, and connecting our members to new opportunities and each other. As a 501(c)(3) non-profit, we provide resources and mentorship to ensure career access for the next generation of LGBTQ youth and provide web services to LGBTQ activists around the world.

Join GridGain solution architect Dani Traphagen at the next Nike Tech Talks! Dani will introduce the many components of the open-source Apache Ignite and the ideal use cases.

Food and beverages will be served at the event and there will be time to network before and after the talk.

Join Microsoft senior cloud developer advocate Paige Bailey at the next Nike Tech Talks on March 22! Paige will give a talk titled, Predicting Clothing Styles with Deep Transfer Learning.

Food and beverages will be served and there will be time to network before and after the talk.

RSVP: https://niketechtalk-mar2018.splashthat.com/

ABSTRACT: In this talk, we'll use image recognition to take an existing deep learning model and adapt it to a specialized domain (namely: guessing whether articles of clothing are preppy, sporty, punk, etc.). Instead of using a more intensive data classifier, like a Residual Network, we'll use deep transfer learning to overcome a data scarcity problem and build on top of an existing model.

Once the transfer learning model has been trained, we'll pack it up into a dockerized container (specifying inputs and outputs, as well as a score.py file), and then call it as a web service. We will also discuss a #DataOps process for refreshing the model as trends change over time.

Join Cornelia Davis, Pivotal Sr. Director of Technology, at the next Nike Tech Talks on April 12! Cornelia will give a talk titled, Turning Request/Response on Its Head.

Food and beverages will be served and there will be time to network before and after the talk.

https://niketechtalks-april2018.splashthat.com/

Join Nike Digital for the next event in our Nike Tech Talks series on Thurs., May 17 from 4:30 - 6:30 p.m. at the Nike Decathlon Club Cafe.

Stephanie Hulburt, Graphics Engineer & Co-Founder of Binomial, will give a talk on Performance in VR & Emerging Tech.

Enjoy snacks and beverages as you network with fellow tech enthusiasts from Nike and beyond. Please feel free to invite friends and colleagues to attend this event.

Join Eric Baer, Director of Software Development at Formidable, Inc., at the next Nike Tech Talks on June 14! Eric will give a talk on The Evolution of API Design from RPC to GraphQL. Food and beverages will be served, and there will be time to network before and after the talk.

About Eric: Eric has been developing products for over ten years in everything from embedded systems for high-end audio products to high-traffic APIs in Java. For the past six years, Eric has developed a deep specialization in JavaScript and the associated ecosystem. In his current role, Eric is an O'Reilly author, a conference speaker and Director of Software Development at both Formidable and at Livestock Nutrition Center, where he is driving large projects and writing software around Babel, GraphQL and i18n.

About the Talk: Over the last 60 years, API designs have changed to respond to everything from new network topologies and new languages, to the pressures of managing ever larger code bases. Today’s most popular API pattern, REST, was developed in a time where the cost of making API requests was plummeting. At the time, bandwidth was getting cheaper, latency was dropping, and the computing power of devices was still tracking Moore’s Law. Mobile turned this on its head. The environments in which apps and APIs need to perform today have effectively regressed a decade.

This talk will explore some of the new client-server interaction models that address today’s pressures and use history to understand the tradeoffs that we made at the transition between the previous designs. Eric will introduce major tools that are attempting to change the API landscape including GraphQL and Falcor. Since GraphQL is the dominant technology in this space, he will examine some of its functionality, touch on some of its syntax and present a live coding demo that shows off a GraphQL server from 0 to 1. Demonstrating a complete implementation in under 10 minutes will give a strong sense of what’s possible, and what kind of complexity burden a tool like this would impose. Spoiler: There is no silver bullet.

Join Alice Goldfuss, Site Reliability Engineer, at the next Nike Tech Talks on August 9. Alice will give a talk titled, The Container Operator’s Manual.

Enjoy snacks and beverages, as you network with fellow tech enthusiasts before and after the talk.

Lean more about the talk and RSVP at: https://niketechtalksaug2018.splashthat.com/.

Join Beth Long, DevOps Solutions Strategist at New Relic, at the Nike Tech Talks on March 14. Beth will give a talk titled, Brains, Bytes & Blowups: How Humans Learn to Keep Complex Systems Alive.

Enjoy snacks and beverages, as you network with fellow tech enthusiasts before and after the talk.

Abstract: As software systems become more complex, we look for strategies to move faster and produce more reliable systems. Yet the price of success is new and more challenging failures. If failure is inevitable, how do we cope? How do we learn from incidents and other types of failure? And how do our ways of collaborating shape the systems we create?

Bio: Beth Long is a software engineer who sneaked into a solutions strategist role at New Relic. Many years ago, she abandoned a potential career as a rocket scientist to tinker with websites. She has written, tested, broken, rescued, and taught code. She's the project lead for New Relic's collaboration with the SNAFUcatchers research project, investigating how tech companies cope with complexity and learn from incidents, a project which has caused her to randomly point and declare, "joint cognitive system!"

Join Allison Smith, Netflix Globalization Innovation Manager, and Dr. Rohit Puri, Netflix Engineering Manager of Cloud Media Systems, at the Nike Tech Talks on May 16. They will give a talk titled, "Best Practices in Timed Text Localization."

Enjoy snacks and beverages, as you network with fellow tech enthusiasts before and after the talk.

Abstract: Netflix is the world's leading internet entertainment service with over 148 million paid memberships in over 190 countries enjoying TV series, documentaries and feature films across a wide variety of genres and languages. Since Netflix first began its international expansion in 2010, localization has played a critical role in bringing joy to global audiences. This presentation will cover the best practices learned through developing and refining a Unicode based timed text processing pipeline, as well as the role of various timed text formats and standards in helping us realize this scalable end-to-end pipeline. In addition, we will discuss the business and tooling strategy for creating and reviewing localized content at scale. This overview will provide an understanding of how the localization ecosystem balances the challenges of scale while prioritizing unique aspects of audiences and languages.

Join us for the Nike Tech Talks! Amanda Casari, Google Cloud Engineering Manager, will give a talk titled, "From Zero to A^X: Scaling Data Science Teams."

Enjoy snacks and beverages, as you network with fellow tech enthusiasts before and after the talk.

More info: https://niketechtalks-august2019.splashthat.com/

Join us for the Nike Tech Talks! Abel Wang, Principal Cloud and DevOps Lead at Microsoft, will be presenting "Real World DevOps"

Enjoy snacks and beverages, as you network with fellow tech enthusiasts before and after the talk.

More details and RSVP at https://niketechtalksnov19.splashthat.com/

The rise of machine learning (ML) and artificial intelligence (AI) have instigated significant interests in developing domain specific integrated circuits and architectures that can support the computational demands of AI. These chips are commonly known as AI chips. AI chips, both for training and inferencing, have emerged out to be new areas of research and commercialization in semiconductor industry. Particularly, increasing emphasis has been placed on developing low-power AI chips for edge applications where AI can be local, distributed, and seamlessly integrated in sensors or other internet of things (IoT) devices for building naturally-autonomous systems. On the other-hand, globalization of semiconductor ecosystem has led to an era where achieving dominance on Microelectronics supply chain has become as exciting as the famous series “Game of Thrones” for not only the companies but also the countries. Furthermore, the end of Moore’s Law of Scaling of traditional semiconductor transistors has added the climax to this situation as the development and manufacturing of advanced process nodes for the next generation of logic and memory devices get expensive driving most semiconductor industry in the US to be fabless. Interestingly, advanced process nodes such as FINFETS, 3D Transistors, RRAMs/Memristors, and 3D/Monolithic integration and packaging approaches provide unsurpassed opportunities to achieve the much desired On-Chip AI along with the primitives for implementing Hardware Security, and Trust into the integrated circuits. This talk will review some of these technologies and our research efforts in these areas.

The UTxO (unspent transaction output) model is the underlying data structure of Bitcoin, which has since been extended to the Extended UTxO model.

It exists in code, but what does it mean? I will give a novel mathematical model based on some strikingly simple type equations which -- for me at least -- make it easier to see what is structurally going on. I will describe how the equations can be used to obtain two further models, one which is more abstract and one which is more concrete:

• A universal algebra axiomatisation, exhibiting Blockchain as an algebraic structure and so implying a general mathematics and specific testable properties against which to verify an EUTxO implementation, and

• An executable Haskell reference implementation

Increasing set of functionalities, network interoperability, and system design complexity have introduced easily exploitable security vulnerabilities in cyber-physical systems (CPS). Furthermore, the tight interaction between information technology and physical world, as well as the rising levels of autonomy, make these systems vulnerable to attacks beyond the standard cyber-attacks; relying exclusively on conventional security techniques may be unfeasible due to resource-constraints and long system lifetime. Consequently, there is a need to change the way we reason about security in CPS, and start designing platform-aware attack-resilient components and architectures capable providing strong safety and performance guarantees even under attack. In this talk, I will present research challenges and our recent efforts in this domain, starting from cyber-physical security techniques that (a) capture effects of attacks on system performance, (b) introduce attack-resilience into components at each level of the autonomy stack, and (c) enable mapping of the desired Quality-of-Control (QoC) under attack guarantees into real-time platform requirements in way that supports design-time tradeoffs between the QoC under attack and security-related overhead. For systems with varying levels of autonomy and human interaction, I will also show how we can exploit human power of inductive reasoning and the ability to provide context, to improve the overall security guarantees. Finally, I will present how we can capture security-related CPS specification as hyperproperties, and introduce statistical model checking methods to check such specifications.

In the real world, people join humanity, grow up trusting very different quorums from one another, and they may change their quorums with time. In technical terms we could call this an open permissionless system with mutable local quorums.

One might expect such a system to be a jumbled disorder — and yet, somehow, it self-organises into uniform areas of fairly stable consensus. One might almost suspect there could be some deep mathematical principles involved!

In this talk I will discuss consensus in a permissionless open system with mutable local quorums, and show how a topological view of the system gives a clean mathematical analysis with surprisingly good explanatory power.

Secure multi-party computation (MPC) allows multiple parties, each holding private data that they are unwilling to share, to collaborate to perform computations over their data, while revealing nothing other than the result. The theory behind secure computation is already 35 years old, but in the last 15 years researchers in the field have demonstrated tremendous improvement in performance. Today, a confluence of factors are driving an increased interest in secure computation, both in the public domain and in industry, including the advancements in MPC mentioned above, the explosion in the volume of private user data being generated, and the advancements in machine learning that are being deployed to leverage that private data.

In this talk, I will give an overview of several of my recent results that has helped scale the performance of secure computation. In the first half of the talk, I will focus on the setting where we have large volumes of data and a secure computation that is out-source to a small number of servers — the Few-PC setting. I will focus on a security relaxation that allows us to improve communication costs asymptotically and concretely for a large class of computations. In the second half of the talk, I will describe several results that allow us to scale MPC to thousands or even millions of parties, by demonstrating a protocol that requires less communication and computation from each participant as the number of participants grows.

Join us this Friday, April 19th, at 1 pm PST for a technical walkthrough of the DSPY library with Chris Thompson.

DSPy is a library released out of Stanford University that aims to completely change the prompting process by treating it less like whack-a-mole and more like training a machine learning model.

In this Talk, Christopher will discuss: - Prompt Engineering - OpenAI Functions - Explanation and demonstration of the DSPy library - Q&A

Currently, Chris works as a Machine Learning Articecht for Insight, a Fortune 500 solutions integrator helping organizations accelerate their digital journey.

Join us Friday, April 19th at 1 pm Pacific Time (2 pm MT, 3 pm CT, 4 pm ET).

Register on Meetup: https://bit.ly/TechTalk419 Register on Eventbrite: https://bit.ly/TechTalkE419

Networking Opportunity: For those seeking valuable connections, this event is your golden ticket. Engage, learn, and expand your network with like-minded tech enthusiasts.

Take this chance to gain insights, ask questions, and connect with like-minded individuals. See you there!

The position of “AI Developer” is a relatively new one. And did you know that they spend less than half their time actually working with AI and writing code? So, what do they spend the rest of their time doing?

Join The Tech Academy at 5:00 p.m. PST (7 CST / 8 EST) for our live online event entitled “A Day in the Life of an AI Developer“ on May 10 (Friday evening), and gain answers to these questions and more.

Erik Gross has been working in tech for decades and at this free workshop, he will “lift the curtain” on the technology sector and AI, and tell you what it’s really like.

Register for this special event now!

Meetup link: https://bit.ly/ErikWorkshop0510 Eventbrite link: https://bit.ly/ErikWorkshop510

Hope to see you there!

Artificial intelligence is quickly taking over all of our lives. Like any tool, it can be used for construction or destruction – good or evil.

On May 25 (Saturday evening) the Co-Founder of The Tech Academy, Erik Gross, will teach students how to leverage AI in order to write and debug effective code. This live online free class will start at 5:00 p.m. PST (7 CST / 8 EST).

Learn about useful tools that will help you on your journey as a technology professional!

Register your attendance for this powerful and useful workshop now!

Meetup link: https://bit.ly/ErikWorkshop0524 Eventbrite link: https://bit.ly/ErikWorkshopE0524

Join The Tech Academy as we create the popular and classic game “Connect 4” using Python! In this free live class, Erik Gross (our Co-Founder) will cover the basics of coding for absolute beginners.

This online workshop will be hosted through Zoom at 5:00 p.m. PST (7 CST / 8 EST), on May 31 (Friday evening).

This free coding class is for people who have never written code before, and in it Mr. Gross will explain every line of code in plain English. All technical terms and concepts will be defined simply. Python is one of the most-used programming languages in the world and you’ll get your feet wet here!

Register for this fun and educational intro to coding class for beginners now!

Meetup link: https://bit.ly/ErikWorkShop0531 Eventbrite link: https://bit.ly/ErikWorkshopE0531

Artificial intelligence is growing in use and power every day. And unfortunately, it is increasingly being used to scam users through complex schemes and even hacking.

In this free workshop, Erik Gross (Co-Founder of The Tech Academy) will give students tools and resources to protect themselves from AI. He will also show you how to recognize if something was generated by a human or artificial intelligence.

Join The Tech Academy on Zoom at 5:00 p.m. PST (7 CST / 8 EST) for this live online event on June 7 (Friday evening).

Register for this special and useful event now!

Meetup link: https://bit.ly/ErikWorkShop0607 Eventbrite link: https://bit.ly/ErikWorkshopE0607

Learn how to create your very own text-based adventure game, similar to the classic game Zork, at this live class delivered by the Co-Founder of The Tech Academy.

This online workshop will teach the basics of the popular programming language Python, and you can join us on Zoom at 5:00 p.m. PST (7 CST / 8 EST), on June 14 (Friday evening).

This live class is for people who have never written code before, and in it Mr. Gross will explain every line of code in plain English. All technical terms and concepts will be defined simply. Python is one of the most-used programming languages in the world and you’ll get a taste of it here!

Confirm your attendance now for this fun and educational Intro to Python coding class!

Meetup link: https://bit.ly/ErikWorkShop0614 Eventbrite link: https://bit.ly/ErikWorkshopE0614

Join The Tech Academy on Zoom at 5:00 p.m. PST (7 CST / 8 EST) for our live online event entitled “Using ChatGPT to Prepare for Interviews” on June 21 (Friday evening).

The host of this webinar is Erik Gross (our Co-Founder) and he is not only an experienced software developer who has been working in tech for decades, he is an expert in AI and leveraging ChatGPT. At this free workshop, we will cover how to ace interviews with AI. And don’t worry, no cheating is involved! This will be ethical usage of ChatGPT.

Register for this valuable, yet free, event now!

Meetup link: https://bit.ly/ErikWorkShop0621 Eventbrite link: https://bit.ly/ErikWorkshopE0621

Join The Tech Academy at this free, online intro to coding class, hosted live by Erik Gross (our Co-Founder), where he will show you how to create the game “Hangman” using one of the top programming languages in the world: Python.

The class will be held on Zoom on June 28 (Friday evening) starting at 5:00 p.m. PST (7 CST/8 EST).

This workshop is for people who have never written code before, and in it, Mr. Gross will explain every line of code in plain English. All technical terms and concepts will be defined simply.

Register now for The Tech Academy’s fun, simple and educational Intro to Python coding class!

Meetup link: https://bit.ly/ErikWorkShop0628 Eventbrite link: https://bit.ly/ErikWorkshopE0628

Come join The Tech Academy at this very special free introductory online coding class, delivered by Senior-Level Software Developer, and our Co-Founder (Erik Gross). In it, Erik will show you how to build a “Tic-Tac-Toe” video game using the popular programming language: Python.

Attend on Zoom at 5:00 p.m. PST (7 CST / 8 EST), on July 12 (Friday evening).

This live Python class is for people who have never written code before, and in it Mr. Gross will explain every line of code in plain English. All technical terms and concepts will be defined simply. Python is one of the most-used programming languages in the world and you’ll get a taste of it here!

Confirm your attendance now at this fun and very special Intro to coding class!

Meetup link: https://bit.ly/Erikworkshop0712 Eventbrite link: https://bit.ly/ErikworkshopE0712

Before you hit "Create Pull Request," are you truly ready?

In this insightful talk, Matthew Singleton, The Tech Academy Graduate, will share his journey from rapid-fire coding to mastering the art of thoughtful development. Inspired by Abraham Lincoln's famous quote, "Give me six hours to chop down a tree and I will spend the first four sharpening the axe," Matthew will discuss the transformative habits that have shaped his approach to coding. You'll learn how self-reviews, functional testing, and collaboration with teammates can elevate your coding practice.

Join us on September 6 at 1 PM PT to discover how slowing down can lead to greater speed and precision in your coding journey.

Why Attend?

Adopt practices that reduce bugs and ensure robust code to enhance code quality

Learn practical tips and gain insights from Matthew Singleton on self-reviews and testing.

Discover how thoughtful coding leads to faster, better results leading to optimized workflow.

Whether you're a seasoned developer or just starting out, this talk will offer valuable insights into writing your best code yet.

See you on Friday!

Unlock Your Future with Kevin Zaw: The Tech Talk You Can’t Afford to Miss!

This Friday, 13 of September at 1 PM, dive into the world of tech innovation with Kevin Zaw, a trailblazer who turned his start at The Tech Academy into a stellar career at industry giants like Oracle and Salesforce. With 5 years of high-impact experience, Kevin has become a master in Revenue Transformation, Pre-Sales, and AI - and he’s ready to show you how to do the same!

Here’s Why You Need to Be There:

Discover how Kevin transforms complex challenges into breakthrough solutions with his cutting-edge approach. Get the insider tactics that have helped Kevin drive success at some of the biggest names in tech. Learn how to stay ahead of the curve by mastering AI and positioning yourself at the forefront of industry trends. This isn’t just another talk, it’s your chance to learn from a true industry expert who’s been where you are and knows exactly how to rise to the top.

Don’t miss out on the opportunity to elevate your tech career!